COMMENT ⊗   VALID 00003 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	1. Thinking about X.  Seeks the nearest unicorn.
C00003 00003	1. ∃P1.(denot P1 = ortcutt ∧ true Believe(Ralph, Isspy P1))
C00004 ENDMK
C⊗;
1. Thinking about X.  Seeks the nearest unicorn.

2. John thantebelieves ∀x. man(x) ⊃ mortal(x)
so that if he ever comes to actively believ man(Socrates)
he will come to believe mortal(Socrates).

The concept must retain its structure as a quantified
implication.

On the whole, the advantages seem to favor keeping
concepts with distinct structures as distinct objects.

What are the rules for know

axiom knoweq:
∀P X1 X2 w.(true(w,Know(P,X1)) ∧ true(w,(Know(P,X2))
∧ true(w,Equal(X1,X2)) ⊃ true(w,K(P,Equal(X1,X2))))
;;
1. ∃P1.(denot P1 = ortcutt ∧ true Believe(Ralph, Isspy P1))